00100	GIVEAX(SCW1,(∀ W)(SCWORLD W ⊃ ISSETSET BASIS W
00200		∧ (∀ U)(U ε BASIS W ⊃ ¬(UUεU))));
00300	
00400	GIVEAX(SCW2,(∀ W)(SCWORLD W ⊃ (∀ U)(U ε BASIS W
00500				⊃ TORD U ε ORDERINGS W)));
00600	
00700	GIVEAX(SCW3,(∀ W)(SCWORLD W ∧ R1 ε ORDERINGS W
00800		∧ R2 ε ORDERINGS W ⊃ (R1→→R2) ε ORDERINGS W));
00900	
01000	GIVEAX(SCW4,(∀ W)(∀ Z)(SCWORLD W ∧ (∀ U)(U ε BASIS W
01100		⊃ TORD U ε Z) ∧ (∀ R1)(∀ R2)(R1εZ ∧ R2εZ
01200			⊃ (R1→→R2)εZ) ⊃ (ORDERINGS W ⊂ Z)));
01300	
01400	GIVEAX(SCW5,(∀ W)(∀ S)(∀ V)(∀ R)(SCWORLD W ∧ S ε STATES W
01500		∧ R ε ORDERINGS W ∧ V ε TERMS(R,W) ⊃
01600			C(V,S) ε DOMAIN R));
01700	
01800	GIVEAX(SCW6,(∀ W)(SCWORLD W ⊃ STATES W ≠ NULLSET));
01900	
02000	GIVEAX(SCW7,(∀ W)(∀ R)(SCWORLD W ∧ R ε ORDERINGS W
02100		⊃ INFINITE VARS R ∧ VARS R ⊂ TERMS(R,W)));
02200	
02300	GIVEAX(SCW8,(∀ W)(∀ R)(∀ X)(SCWORLD W ∧ R ε ORDERINGS W
02400		∧ X ε DOMAIN R ⊃ MKCONST X ε TERMS(R,W)
02500			∧ ISCONST MKCONST X
02600			∧ VALUE MKCONST X = X
02700			∧ (∀ S)(S ε STATES W ⊃ C(MKCONST X,S) = X)));
02800	
02900	GIVEAX(SCW9,(∀ W)(∀ R)(∀ V)(∀ X)(∀ S)(SCWORLD W ∧ R ε ORDERINGS W
03000		∧ V ε VARS R ∧ X ε DOMAIN R ∧ S ε STATES W
03100			⊃
03200		A(V,X,S) ε STATES W
03300		∧ C(V,A(V,X,S)) = X
03400		∧ (∀ R1)(∀ V1)(R1 ε ORDERINGS W ∧ V1 ε VARS R
03500			∧ V1≠V ⊃ C(V1,A(V,X,S)) = C(V1,S))));
03600	
03700	GIVEAX(SCW10,(∀ W)(∀ R)(∀ V)(SCWORLD W ∧ R ε ORDERINGS W
03800		∧ V ε VARS R ⊃ FREEVARS V = UNITSET V));
03900	
04000	GIVEAX(SCW11,(∀ W)(∀ R)(∀ E)(SCWORLD W ∧ R ε ORDERINGS W
04100		∧ E ε TERMS(R,W) ∧ ISCONST E
04200		⊃ FREEVARS E = NULLSET));
04300	
04400	GIVEAX(SCW12,(∀ W)(∀ R1)(∀ E1)(∀ R2)(∀ E)(∀ S)(SCWORLD W
04500		∧ R1 ε ORDERINGS W ∧ E1 ε TERMS(R1,W)
04600		∧ R2 ε ORDERINGS W ∧ E ε TERMS(R1→→R2,W)
04700		∧ S ε STATES W
04800				⊃
04900		α(E,E1) ε TERMS(R2,W)
05000		∧ FREEVARS α(E,E1) = FREEVARS E ∪ FREEVARS E1
05100		∧ C(α(E,E1),S) = β(C(E,S),C(E1,S))));
05200	
05300	GIVEAX(SCW13,(∀ W)(∀ R1)(∀ R2)(∀ V1)(∀ E2)(∀ S)(SCWORLD W
05400		∧ R1 ε ORDERINGS W ∧ R2 ε ORDERINGS W
05500		∧ V1 ε VARS R1 ∧ V2 ε TERMS(R2,W)
05600		∧ S ε STATES W
05700				⊃
05800		LAM(V1,E2) ε TERMS(R1→→R2,W)
05900		∧ FREEVARS LAM(V1,E2) = FREEVARS(E2)-UNITSET(V1)
06000		∧ (∀ X)(X ε DOMAIN R1 ⊃ β(C(LAM(V1,E2),S),X)
06100			= C(E2,A(V1,X,S)))));
06200	
06300	GIVEAX(SCW14,(∀ W)(∀ R)(∀ F)(∀ V)(∀ S)(SCWORLD W ∧ R ε ORDERINGS W
06400		∧ F ε TERMS(R→→R,W) ∧ V ε VARS R ∧ S ε STATES W
06500				⊃
06600		MU(V,F) ε TERMS(R,W)
06700		∧ FREEVARS MU(V,F) = FREEVARS(F)-UNITSET(V)
06800		∧ C(MU(V,F),S) = β(C(F,S),C(MU(V,F),S))
06900		∧ (∀ X)(X ε DOM R ∧ C(X,S) = β(C(F,S),C(X,S))
07000				⊃ ββ(C(MU(V,F),S),R,X))));
07100	
07200	GIVEAX(SCW15,(∀ W)(∀ E1)(∀ E2)(∀ R)(SCWORLD W ∧ R ε ORDERINGS W
07300		∧ E1 ε TERMS(R,W) ∧ E2 ε TERMS W
07400		∧ (∀ S)(S ε STATES W ⊃ C(E1,S) = C(E2,S))
07500				⊃ E1 = E2));
07600	
07700	GIVEAX(SCW16,(∀ W)(∀ R)(∀ P)(∀ E1)(∀ E2)(
07800		SCWORLD W ∧ R ε ORDERINGS W ∧ P ε TERMS(TORD TV,W)
07900		∧ E1 ε TERMS(R,W) ∧ E2 ε TERMS(R,W)
08000				⊃
08100		IFF(P,E1,E2) ε TERMS(R,W)
08200		∧ (∀ S)(S ε STATES W ⊃ C(IFF(P,E1,E2),S) =
08300			IF C(P,S)=TRUE THEN C(E1,S)
08400			ELSE IF C(P,S)=FALSE THEN C(E2,S)
08500			ELSE UU)));
08600	
08700	GIVEAX(SCW17,(∀ W)(∀ R)(∀ E)(∀ S1)(∀ S2)
08750		(SCWORLD W ∧ R ε ORDERINGS W
08800		∧ E ε TERMS(R,W) ∧ S1 ε STATES W
08900		∧ S2 ε STATES W ∧ (∀ V)(V ε FREEVARS E
09000			C(V,S1)=C(V,S2))
09100		⊃ C(E,S1) = C(E,S2)));
09200	COMMENT - States giving the same value to all the free variables
09300	of at term give the same value to the term. ;
09400	
09500	GIVEAX(SCW18,(∀ W)(∀ R)(SCWORLD W ∧ R ε ORDERINGS W
09600		⊃ INFINITE VARS(R,W)));
09700	COMMENT - There are infinitely many variables of all types. ;
     

00100	END;